#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#include "../model/datatypes.h"
#include "../model/globals.h"
#include "../model/memory_utils.h"
#include "../model/internal_kb.h"
#include "normalized_datatypes.h"
#include "normalization_globals.h"
#include "print_utils.h"
#include "utils.h"
#include "locals.h"

int normalized_atomic_concept_count = 0;
int normalized_atomic_role_count = 0;
int generated_atomic_concept_count = 0;
int generated_exists_restriction_count = 0;
int generated_subclass_axiom_count = 0;
int generated_subrole_axiom_count = 0;
int singleton_premise_count = 0;
int max_lhs_size = 0;
int max_rhs_size = 0;
int cum_lhs_size = 0;
int cum_rhs_size = 0;
NormalizedConcept** normalized_atomic_concepts = NULL;
NormalizedRole** normalized_atomic_roles = NULL;
Pvoid_t normalized_exists_restrictions = (Pvoid_t) NULL;
Pvoid_t normalized_conjunctions = (Pvoid_t) NULL;
// NormalizedConcept** normalized_atomic_concepts_left = NULL;
// int normalized_atomic_concepts_left_count = 0;
Pvoid_t normalized_atomic_concepts_left = (Pvoid_t) NULL;

NormalizedTBox normalized_tbox;
// judy arrays for storing generated atomic concepts information
Pvoid_t generated_atomic_concepts_right = (Pvoid_t) NULL;
Pvoid_t generated_atomic_concepts_left = (Pvoid_t) NULL;

int generated_atomic_concepts_left_count = 0;
int generated_atomic_concepts_right_count = 0;


/*
enum axiom_side {
	LEFT_HANDSIDE, RIGHT_HANDSIDE
};
*/


NormalizedConcept* create_normalized_conjunction(NormalizedConcept** conjuncts, int size) {
	NormalizedConcept* c;
	int i, judy_return;

	c = get_normalized_conjunction(conjuncts, size);
	if (c == NULL) {
		c = (NormalizedConcept*) malloc(sizeof(NormalizedConcept));
		assert(c != NULL);
		c->type = NORMALIZED_CONJUNCTION;
		c->description.conj = (NormalizedConjunction*) malloc(sizeof(NormalizedConjunction));
		assert(c->description.conj != NULL);

		c->description.conj->conjuncts = (Pvoid_t) NULL;
		for (i = 0; i < size; ++i) {
			J1S(judy_return, c->description.conj->conjuncts, (Word_t) conjuncts[i]);
			if (judy_return == JERR) {
				fprintf(stderr,"could not add conjunct, aborting!\n");
				exit(-1);
			}
		}
		put_normalized_conjunction(c);
	}
	return c;
}

NormalizedConcept* create_normalized_atomic_concept(Concept* c) {
	NormalizedConcept* ac = normalized_atomic_concepts[c->description.atomic->id];
	// first check if it already exists
	if (ac != NULL)
		return ac;

	ac = (NormalizedConcept*) malloc(sizeof(NormalizedConcept));
	assert(ac != NULL);
	ac->type = NORMALIZED_ATOMIC_CONCEPT;
	ac->description.atomic = (NormalizedAtomicConcept*) malloc(sizeof(NormalizedAtomicConcept));
	assert(ac->description.atomic != NULL);
	ac->description.atomic->id = c->description.atomic->id;
	// name of the original atomic concept is reused. shouldn't be freed!
	ac->description.atomic->name = c->description.atomic->name;
	ac->description.atomic->subsumers = (Pvoid_t) NULL;
	// ac->singleton_premises_count = 0;
	// ac->singleton_premises = NULL;
	ac->containing_premises_count = 0;
	ac->containing_premises = NULL;
	ac->description.atomic->axioms_to_process = (Pvoid_t) NULL;
	ac->description.atomic->number_of_filler_of = 0;
	ac->description.atomic->filler_of = NULL;

	normalized_atomic_concepts[ac->description.atomic->id] = ac;

	return ac;
}

// TODO:
NormalizedRole* create_normalized_atomic_role(Role* r) {
	NormalizedRole* ar = normalized_atomic_roles[r->description.atomic->id];
	if (ar != NULL)
		return ar;

	ar = (NormalizedRole*) malloc(sizeof(NormalizedRole));
	assert(ar != NULL);
	ar->type = NORMALIZED_ATOMIC_ROLE;
	ar->description.atomic = (NormalizedAtomicRole*) malloc(sizeof(NormalizedAtomicRole));
	assert(ar->description.atomic != NULL);
	ar->description.atomic->id = r->description.atomic->id;
	ar->description.atomic->name = r->description.atomic->name;
	ar->description.atomic->subsumers = NULL;
	ar->description.atomic->subsumees = NULL;

	normalized_atomic_roles[ar->description.atomic->id] = ar;
	
	return ar;
}

NormalizedConcept* create_new_normalized_atomic_concept(enum axiom_side side) {
	char name[24];
	NormalizedConcept* c;
	NormalizedConcept** tmp;

	c = (NormalizedConcept*) malloc(sizeof(NormalizedConcept));
	assert(c != NULL);
	c->type = NORMALIZED_ATOMIC_CONCEPT;
	c->description.atomic = (NormalizedAtomicConcept*) malloc(sizeof(NormalizedAtomicConcept));
	assert(c->description.atomic != NULL);

	switch (side) {
		case LEFT_HANDSIDE:
			snprintf(name,24,"_CREATED_L_%d",generated_atomic_concepts_left_count);
			// c->description.atomic->id = generated_atomic_concepts_left_count;
			c->description.atomic->id = generated_atomic_concepts_left_count + generated_atomic_concepts_right_count;
			++generated_atomic_concepts_left_count;
			break;
		case RIGHT_HANDSIDE:
			snprintf(name,24,"_CREATED_R_%d",generated_atomic_concepts_right_count);
			// c->description.atomic->id = generated_atomic_concepts_right_count;
			c->description.atomic->id = generated_atomic_concepts_left_count + generated_atomic_concepts_right_count;
			++generated_atomic_concepts_right_count;
			break;
	}
	c->description.atomic->name = (char*) malloc((strlen(name) + 1) * sizeof(char));
	assert(c->description.atomic->name != NULL);
	strcpy(c->description.atomic->name, name);
	c->description.atomic->subsumers = (Pvoid_t) NULL;
	// c->singleton_premises_count = 0;
	// c->singleton_premises = NULL;
	c->containing_premises_count = 0;
	c->containing_premises = NULL;
	c->description.atomic->axioms_to_process = (Pvoid_t) NULL;
	c->description.atomic->number_of_filler_of = 0;
	c->description.atomic->filler_of = NULL; 

	tmp = realloc(normalized_atomic_concepts, (normalized_atomic_concept_count + 1) * sizeof(NormalizedConcept*));
	assert(tmp != NULL);
	normalized_atomic_concepts = tmp;
	normalized_atomic_concepts[normalized_atomic_concept_count] = c;
	++normalized_atomic_concept_count;
	// for normalization stats
	// ++generated_atomic_concept_count;

	return c;
}

void add_normalized_axiom(NormalizedAxiom* ax, NormalizedTBox* n_tbox) {
	
	NormalizedAxiom** tmp;
	
	tmp = realloc(n_tbox->axioms, (n_tbox->axiom_count + 1) * sizeof(NormalizedAxiom*));
	assert(tmp != NULL);
	n_tbox->axioms = tmp;
	n_tbox->axioms[n_tbox->axiom_count] = ax;
	++(n_tbox->axiom_count);
}


NormalizedAxiom* create_normalized_subclass_axiom(NormalizedConcept* lhs, NormalizedConcept* rhs) {
	int conjunct_count;

 	NormalizedAxiom* ax = (NormalizedAxiom*) malloc(sizeof(NormalizedAxiom));
	assert(ax != NULL);
	ax->type = NORMALIZED_SUBCLASS_AX;
	ax->body.subclass_ax = (NormalizedSubClassAxiom*) malloc(sizeof(NormalizedSubClassAxiom));
	assert(ax->body.subclass_ax != NULL);
	ax->body.subclass_ax->lhs = lhs;
	ax->body.subclass_ax->rhs = rhs;

	// for normalization stats
	if (lhs->type == NORMALIZED_CONJUNCTION) {
		// get the size of conjunction
		J1C(conjunct_count,lhs->description.conj->conjuncts,0,-1);
		cum_lhs_size += conjunct_count;
		if (conjunct_count > max_lhs_size) 
			max_lhs_size = conjunct_count;
	}
	else {
		++singleton_premise_count;
		max_lhs_size = 1;
		cum_lhs_size += 1;
	}
	if (rhs->type == NORMALIZED_CONJUNCTION) {
		// get the size of conjunction
		J1C(conjunct_count,rhs->description.conj->conjuncts,0,-1);
		cum_rhs_size += conjunct_count;
		if (conjunct_count > max_rhs_size) 
			max_rhs_size = conjunct_count;
	}
	else
		cum_rhs_size += 1;
		

	++generated_subclass_axiom_count;

        return ax;
}


NormalizedConcept* normalize_concept(Concept* c, enum axiom_side side,NormalizedTBox* n_tbox) {
	int i;
	NormalizedConcept* normalized_conjunction;
	NormalizedConcept** conjuncts;
	NormalizedConcept* normalized_atomic_concept;
	NormalizedRole* normalized_atomic_role;
	// int judy_return;
	NormalizedConcept* generated_atomic_concept;
	NormalizedConcept* normalized_filler;
	switch (c->type) {
		case ATOMIC_CONCEPT:
			// atomic concepts in the original TBox are also
			// used in the normalized axioms
			// return (NormalizedConcept*) c;
			normalized_atomic_concept = create_normalized_atomic_concept(c);
			if (side == LEFT_HANDSIDE)
				add_to_normalized_atomic_concepts_left(normalized_atomic_concept);
			return normalized_atomic_concept;
			break;
		case CONJUNCTION:
			/*
			normalized_conjunction = create_normalized_conjunction();
			for (i = 0; i < c->description.conj->count; ++i) {
				J1S(judy_return,normalized_conjunction->description.conj->conjuncts,(Word_t) normalize_concept(c->description.conj->conjuncts[i], side,n_tbox));
				if (judy_return == JERR) {
					fprintf(stderr,"could not add conjunct, aborting!\n");
					exit(-1);

				}
			}
			return normalized_conjunction;
			*/
			conjuncts = (NormalizedConcept**) malloc(c->description.conj->count * sizeof(NormalizedConcept*));
			assert(conjuncts != NULL);
			for (i = 0; i < c->description.conj->count; ++i) {
				conjuncts[i] = normalize_concept(c->description.conj->conjuncts[i], side, n_tbox);
			}
			normalized_conjunction = create_normalized_conjunction(conjuncts, c->description.conj->count);
			free(conjuncts);
			return normalized_conjunction;
			break;
		case EXISTENTIAL_RESTRICTION:
			normalized_atomic_role = create_normalized_atomic_role(c->description.exists->role);
			if (c->description.exists->filler->type == ATOMIC_CONCEPT) {
				normalized_atomic_concept = create_normalized_atomic_concept(c->description.exists->filler);
				// if (side == LEFT_HANDSIDE)
				// 	add_to_normalized_atomic_concepts_left(normalized_atomic_concept);
				// here lookup the concept, if not found create a normalized existential restriction
				return create_normalized_exists(normalized_atomic_role,normalized_atomic_concept);
			}
			else {
				normalized_filler = normalize_concept(c->description.exists->filler, side,n_tbox);
				generated_atomic_concept = get_generated_atomic_concept(normalized_filler, side);
				if (generated_atomic_concept == NULL) {
					generated_atomic_concept = create_new_normalized_atomic_concept(side);
					put_generated_atomic_concept(generated_atomic_concept, normalized_filler, side);
					switch (side) {
						case LEFT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(normalized_filler, generated_atomic_concept), n_tbox);
							break;
						case RIGHT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(generated_atomic_concept, normalized_filler), n_tbox);
							add_to_normalized_atomic_concepts_left(generated_atomic_concept);
							break;
						default:
							fprintf(stderr, "axiom side undefined, aborting\n");
							exit(-1);
					}
				}
/*
				normalized_filler = normalize_concept(c->description.exists->filler, side,n_tbox);
				generated_atomic_concept = get_generated_atomic_concept(normalized_filler);
				// check if an atomic concept for this complex filler already generated
				if (generated_atomic_concept == NULL) {
					generated_atomic_concept = create_new_normalized_atomic_concept();
					put_generated_atomic_concept(generated_atomic_concept, normalized_filler, side);
					// here create a new subclass axiom
					switch (side) {
						case LEFT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(normalized_filler, generated_atomic_concept), n_tbox);
							add_to_normalized_atomic_concepts_left(generated_atomic_concept);
							break;
						case RIGHT_HANDSIDE:
							add_normalized_axiom(create_normalized_subclass_axiom(generated_atomic_concept, normalized_filler), n_tbox);
							break;
						default:
							fprintf(stderr, "axiom side undefined, aborting\n");
							exit(-1);
					}
				}
				else {
					// now check whether it was generated for the same side previously
					if (!generated_atomic_concept_for_side(generated_atomic_concept, side)) {
						put_generated_atomic_concept_side(generated_atomic_concept, side);
						if (side == LEFT_HANDSIDE) {
							add_normalized_axiom(create_normalized_subclass_axiom(normalized_filler, generated_atomic_concept), n_tbox);
						}
						else if (side == RIGHT_HANDSIDE) {
							add_normalized_axiom(create_normalized_subclass_axiom(generated_atomic_concept, normalized_filler), n_tbox);
						}
						else {
							fprintf(stderr, "axiom side undefined, aborting\n");
							exit(-1);
						}
					}
				}
*/
				return create_normalized_exists(normalized_atomic_role, generated_atomic_concept);

			}
			break;
		default:
			fprintf(stderr, "unknown concept type, aborting\n");
			exit(-1);
	}
}

NormalizedAxiom* create_normalized_subrole_axiom(NormalizedRole* lhs, NormalizedRole* rhs) {
        NormalizedAxiom* ax = (NormalizedAxiom*) malloc(sizeof(NormalizedAxiom));
        assert(ax != NULL);
        ax->type = NORMALIZED_SUBROLE_AX;
        ax->body.subrole_ax = (NormalizedSubRoleAxiom*) malloc(sizeof(NormalizedSubRoleAxiom));
        assert(ax->body.subrole_ax != NULL);
        ax->body.subrole_ax->lhs = lhs;
        ax->body.subrole_ax->rhs = rhs;

	++generated_subrole_axiom_count;

        return ax;
}

void normalize_subclass_axiom(SubClassAxiom* ax, NormalizedTBox* n_tbox) {
	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->lhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->rhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);
}

void normalize_eqclass_axiom(EqClassAxiom* ax, NormalizedTBox* n_tbox) {

/*
	Axiom* tmp;

	tmp = create_subclass_axiom(ax->lhs, ax->rhs);
	normalize_subclass_axiom(tmp->body.subclass_ax, n_tbox);
	
	tmp = create_subclass_axiom(ax->rhs, ax->lhs);
	normalize_subclass_axiom(tmp->body.subclass_ax, n_tbox);

// TODO: free the temporary axioms!
*/
	
/*
	int i, ax_count1, ax_count2;

	ax_count1 = n_tbox->axiom_count;

	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->lhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->rhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);

	ax_count2 = n_tbox->axiom_count;

	for (i = ax_count1; i < ax_count2; ++i)
		add_normalized_axiom(
			create_normalized_subclass_axiom(n_tbox->axioms[i]->body.subclass_ax->rhs, n_tbox->axioms[i]->body.subclass_ax->lhs), n_tbox);
*/
	

	// create and add 2 subclass axioms
	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->lhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->rhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);

	add_normalized_axiom(
		create_normalized_subclass_axiom(
		normalize_concept(ax->rhs, LEFT_HANDSIDE,n_tbox),
		normalize_concept(ax->lhs, RIGHT_HANDSIDE,n_tbox)), n_tbox);

}

void normalize_subrole_axiom(SubRoleAxiom* ax, NormalizedTBox* n_tbox) {
	NormalizedRole* new_role;
	NormalizedRoleComposition* new_composition;

	if (ax->rhs->type != ATOMIC_ROLE) {
		fprintf(stderr,"role compositions on the rhs not supported, aborting!");
		exit(-1);
	}
	switch (ax->lhs->type) {
		case ATOMIC_ROLE:
			add_normalized_axiom(create_normalized_subrole_axiom((NormalizedRole*) ax->lhs, (NormalizedRole*) ax->rhs), n_tbox);
			break;
		case ROLE_COMPOSITION:
			if (ax->lhs->description.role_composition->size == 2) {
				new_role = (NormalizedRole*) malloc(sizeof(NormalizedRole));
				assert(new_role != NULL);	
				new_role->type = NORMALIZED_ROLE_COMPOSITION;

				new_composition = (NormalizedRoleComposition*) malloc(sizeof(NormalizedRoleComposition));
				assert(new_composition != NULL);
				new_composition->role1 = ax->lhs->description.role_composition->roles[0]->description.atomic->id;
				new_composition->role2 = ax->lhs->description.role_composition->roles[1]->description.atomic->id;

				new_role->description.role_comp = new_composition;
			}	
			// TODO:
			else {
				fprintf(stderr, "TODO: subrole axiom normalization!");
			}
			break;
		default:
			fprintf(stderr,"unknown role type, aborting\n");
			exit(-1);

	}
		
}

void normalize_tbox(TBox tbox, NormalizedTBox* n_tbox) {
	int i;

	// init normalized_tbox
	normalized_tbox.axiom_count = 0;
	// axioms will be dynamically added
	normalized_tbox.axioms = NULL;

	// first create space for normalized atomic concepts
	normalized_atomic_concept_count = atomic_concept_count;
	normalized_atomic_concepts = (NormalizedConcept**) malloc(normalized_atomic_concept_count * sizeof(NormalizedConcept*));
	assert(normalized_atomic_concepts != NULL);
	for (i = 0; i < atomic_concept_count; ++i) {
		normalized_atomic_concepts[i] = NULL;
	}

	// now create space for normalized atomic roles
	normalized_atomic_role_count = atomic_role_count;
	normalized_atomic_roles = (NormalizedRole**) malloc(normalized_atomic_role_count * sizeof(NormalizedRole*));
	assert(normalized_atomic_roles != NULL);
	for (i = 0; i < atomic_role_count; ++i) {
		normalized_atomic_roles[i] = NULL;
	}

	for (i = 0; i < tbox.axiom_count; ++i) {
		switch (tbox.axioms[i]->type) {
			case EQCLASS_AX:
				normalize_eqclass_axiom(tbox.axioms[i]->body.eqclass_ax, n_tbox);
				break;
			case SUBCLASS_AX:
				normalize_subclass_axiom(tbox.axioms[i]->body.subclass_ax, n_tbox);
				break;
			case SUBROLE_AX:
				normalize_subrole_axiom(tbox.axioms[i]->body.subrole_ax, n_tbox);
				break;
			default:
				fprintf(stderr, "unknown axiom type, aborting\n");
				exit(-1);
		}
		
	}

}
